YES 1.924 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ IFR

mainModule List
  ((delete :: Eq a => a  ->  [a ->  [a]) :: Eq a => a  ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ys if x `eq` y then ys else y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys

is transformed to
deleteBy0 ys y eq x True = ys
deleteBy0 ys y eq x False = y : deleteBy eq x ys



↳ HASKELL
  ↳ IFR
HASKELL
      ↳ BR

mainModule List
  ((delete :: Eq a => a  ->  [a ->  [a]) :: Eq a => a  ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((delete :: Eq a => a  ->  [a ->  [a]) :: Eq a => a  ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule List
  (delete :: Eq a => a  ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy2700), Succ(xy401000)) → new_primPlusNat(xy2700, xy401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy3100), Succ(xy40100)) → new_primMulNat(xy3100, Succ(xy40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy300), Succ(xy4000)) → new_primEqNat(xy300, xy4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(xy30, xy31), @2(xy400, xy401), app(app(ty_@2, cc), cd), ce) → new_esEs(xy30, xy400, cc, cd)
new_esEs1(Right(xy30), Right(xy400), bag, app(ty_Maybe, bbh)) → new_esEs3(xy30, xy400, bbh)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), ba, app(app(app(ty_@3, bd), be), bf)) → new_esEs0(xy31, xy401, bd, be, bf)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, dg, app(app(ty_Either, ee), ef)) → new_esEs1(xy32, xy402, ee, ef)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), app(ty_Maybe, hd), dg, fc) → new_esEs3(xy30, xy400, hd)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), ba, app(ty_[], ca)) → new_esEs2(xy31, xy401, ca)
new_esEs2(:(xy30, xy31), :(xy400, xy401), app(ty_Maybe, bdb)) → new_esEs3(xy30, xy400, bdb)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, dg, app(app(ty_@2, dh), ea)) → new_esEs(xy32, xy402, dh, ea)
new_esEs1(Left(xy30), Left(xy400), app(app(app(ty_@3, hh), baa), bab), hg) → new_esEs0(xy30, xy400, hh, baa, bab)
new_esEs1(Left(xy30), Left(xy400), app(ty_[], bae), hg) → new_esEs2(xy30, xy400, bae)
new_esEs3(Just(xy30), Just(xy400), app(ty_[], beb)) → new_esEs2(xy30, xy400, beb)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), app(ty_Maybe, de), ce) → new_esEs3(xy30, xy400, de)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), app(app(ty_Either, ha), hb), dg, fc) → new_esEs1(xy30, xy400, ha, hb)
new_esEs2(:(xy30, xy31), :(xy400, xy401), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs0(xy30, xy400, bcd, bce, bcf)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), app(ty_[], hc), dg, fc) → new_esEs2(xy30, xy400, hc)
new_esEs1(Right(xy30), Right(xy400), bag, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs0(xy30, xy400, bbb, bbc, bbd)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, app(app(ty_@2, fa), fb), fc) → new_esEs(xy31, xy401, fa, fb)
new_esEs1(Left(xy30), Left(xy400), app(app(ty_Either, bac), bad), hg) → new_esEs1(xy30, xy400, bac, bad)
new_esEs1(Right(xy30), Right(xy400), bag, app(app(ty_Either, bbe), bbf)) → new_esEs1(xy30, xy400, bbe, bbf)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, app(app(app(ty_@3, fd), ff), fg), fc) → new_esEs0(xy31, xy401, fd, ff, fg)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, app(app(ty_Either, fh), ga), fc) → new_esEs1(xy31, xy401, fh, ga)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), ba, app(ty_Maybe, cb)) → new_esEs3(xy31, xy401, cb)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), app(app(ty_@2, gd), ge), dg, fc) → new_esEs(xy30, xy400, gd, ge)
new_esEs3(Just(xy30), Just(xy400), app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs0(xy30, xy400, bde, bdf, bdg)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, app(ty_Maybe, gc), fc) → new_esEs3(xy31, xy401, gc)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, dg, app(ty_Maybe, eh)) → new_esEs3(xy32, xy402, eh)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, app(ty_[], gb), fc) → new_esEs2(xy31, xy401, gb)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, dg, app(app(app(ty_@3, eb), ec), ed)) → new_esEs0(xy32, xy402, eb, ec, ed)
new_esEs1(Right(xy30), Right(xy400), bag, app(app(ty_@2, bah), bba)) → new_esEs(xy30, xy400, bah, bba)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), ba, app(app(ty_Either, bg), bh)) → new_esEs1(xy31, xy401, bg, bh)
new_esEs2(:(xy30, xy31), :(xy400, xy401), app(app(ty_Either, bcg), bch)) → new_esEs1(xy30, xy400, bcg, bch)
new_esEs2(:(xy30, xy31), :(xy400, xy401), bca) → new_esEs2(xy31, xy401, bca)
new_esEs3(Just(xy30), Just(xy400), app(ty_Maybe, bec)) → new_esEs3(xy30, xy400, bec)
new_esEs2(:(xy30, xy31), :(xy400, xy401), app(app(ty_@2, bcb), bcc)) → new_esEs(xy30, xy400, bcb, bcc)
new_esEs3(Just(xy30), Just(xy400), app(app(ty_@2, bdc), bdd)) → new_esEs(xy30, xy400, bdc, bdd)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), df, dg, app(ty_[], eg)) → new_esEs2(xy32, xy402, eg)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), ba, app(app(ty_@2, bb), bc)) → new_esEs(xy31, xy401, bb, bc)
new_esEs2(:(xy30, xy31), :(xy400, xy401), app(ty_[], bda)) → new_esEs2(xy30, xy400, bda)
new_esEs1(Left(xy30), Left(xy400), app(ty_Maybe, baf), hg) → new_esEs3(xy30, xy400, baf)
new_esEs1(Left(xy30), Left(xy400), app(app(ty_@2, he), hf), hg) → new_esEs(xy30, xy400, he, hf)
new_esEs1(Right(xy30), Right(xy400), bag, app(ty_[], bbg)) → new_esEs2(xy30, xy400, bbg)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), app(app(app(ty_@3, cf), cg), da), ce) → new_esEs0(xy30, xy400, cf, cg, da)
new_esEs3(Just(xy30), Just(xy400), app(app(ty_Either, bdh), bea)) → new_esEs1(xy30, xy400, bdh, bea)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), app(app(ty_Either, db), dc), ce) → new_esEs1(xy30, xy400, db, dc)
new_esEs0(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), app(app(app(ty_@3, gf), gg), gh), dg, fc) → new_esEs0(xy30, xy400, gf, gg, gh)
new_esEs(@2(xy30, xy31), @2(xy400, xy401), app(ty_[], dd), ce) → new_esEs2(xy30, xy400, dd)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(xy3, :(xy40, xy41), bb) → new_deleteBy0(xy41, xy40, xy3, new_esEs4(xy3, xy40, bb), bb)
new_deleteBy0(xy10, xy11, xy12, False, ba) → new_deleteBy(xy12, xy10, ba)

The TRS R consists of the following rules:

new_esEs22(xy30, xy400, ty_Integer) → new_esEs14(xy30, xy400)
new_esEs25(xy31, xy401, ty_Ordering) → new_esEs17(xy31, xy401)
new_esEs21(xy31, xy401, ty_Double) → new_esEs13(xy31, xy401)
new_primPlusNat1(Succ(xy2700), Succ(xy401000)) → Succ(Succ(new_primPlusNat1(xy2700, xy401000)))
new_esEs22(xy30, xy400, app(ty_Ratio, bae)) → new_esEs9(xy30, xy400, bae)
new_primEqInt(Pos(Succ(xy300)), Neg(xy400)) → False
new_primEqInt(Neg(Succ(xy300)), Pos(xy400)) → False
new_esEs25(xy31, xy401, ty_Bool) → new_esEs15(xy31, xy401)
new_esEs6(xy30, xy400, app(app(ty_@2, be), bf)) → new_esEs10(xy30, xy400, be, bf)
new_esEs26(xy30, xy400, ty_Double) → new_esEs13(xy30, xy400)
new_esEs26(xy30, xy400, app(app(ty_Either, bfe), bff)) → new_esEs12(xy30, xy400, bfe, bff)
new_esEs25(xy31, xy401, ty_Char) → new_esEs8(xy31, xy401)
new_esEs12(Left(xy30), Left(xy400), ty_@0, cf) → new_esEs7(xy30, xy400)
new_primEqInt(Pos(Zero), Neg(Succ(xy4000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy4000))) → False
new_esEs4(xy3, xy40, ty_Int) → new_esEs18(xy3, xy40)
new_esEs9(:%(xy30, xy31), :%(xy400, xy401), bdb) → new_asAs(new_esEs24(xy30, xy400, bdb), new_esEs23(xy31, xy401, bdb))
new_esEs5([], [], bc) → True
new_esEs4(xy3, xy40, app(app(ty_@2, bdc), bdd)) → new_esEs10(xy3, xy40, bdc, bdd)
new_esEs6(xy30, xy400, ty_Integer) → new_esEs14(xy30, xy400)
new_esEs21(xy31, xy401, ty_Ordering) → new_esEs17(xy31, xy401)
new_esEs26(xy30, xy400, app(ty_Maybe, bfh)) → new_esEs19(xy30, xy400, bfh)
new_esEs23(xy31, xy401, ty_Int) → new_esEs18(xy31, xy401)
new_esEs12(Left(xy30), Left(xy400), ty_Bool, cf) → new_esEs15(xy30, xy400)
new_esEs21(xy31, xy401, app(ty_Maybe, bad)) → new_esEs19(xy31, xy401, bad)
new_esEs19(Just(xy30), Just(xy400), app(app(ty_Either, bcf), bcg)) → new_esEs12(xy30, xy400, bcf, bcg)
new_primMulNat0(Zero, Zero) → Zero
new_esEs26(xy30, xy400, ty_Float) → new_esEs16(xy30, xy400)
new_esEs5(:(xy30, xy31), :(xy400, xy401), bc) → new_asAs(new_esEs6(xy30, xy400, bc), new_esEs5(xy31, xy401, bc))
new_esEs21(xy31, xy401, app(ty_[], bac)) → new_esEs5(xy31, xy401, bac)
new_esEs12(Right(xy30), Right(xy400), eb, ty_Int) → new_esEs18(xy30, xy400)
new_esEs20(xy32, xy402, ty_Double) → new_esEs13(xy32, xy402)
new_esEs21(xy31, xy401, ty_Integer) → new_esEs14(xy31, xy401)
new_esEs5([], :(xy400, xy401), bc) → False
new_esEs5(:(xy30, xy31), [], bc) → False
new_esEs20(xy32, xy402, app(app(ty_Either, gg), gh)) → new_esEs12(xy32, xy402, gg, gh)
new_esEs21(xy31, xy401, app(app(ty_Either, baa), bab)) → new_esEs12(xy31, xy401, baa, bab)
new_primPlusNat0(Zero, xy40100) → Succ(xy40100)
new_esEs25(xy31, xy401, ty_Double) → new_esEs13(xy31, xy401)
new_esEs4(xy3, xy40, app(app(app(ty_@3, ff), fg), fh)) → new_esEs11(xy3, xy40, ff, fg, fh)
new_esEs26(xy30, xy400, ty_Int) → new_esEs18(xy30, xy400)
new_esEs26(xy30, xy400, ty_@0) → new_esEs7(xy30, xy400)
new_sr(Neg(xy310), Pos(xy4010)) → Neg(new_primMulNat0(xy310, xy4010))
new_sr(Pos(xy310), Neg(xy4010)) → Neg(new_primMulNat0(xy310, xy4010))
new_esEs13(Double(xy30, xy31), Double(xy400, xy401)) → new_esEs18(new_sr(xy30, xy400), new_sr(xy31, xy401))
new_esEs20(xy32, xy402, ty_Ordering) → new_esEs17(xy32, xy402)
new_esEs6(xy30, xy400, ty_Int) → new_esEs18(xy30, xy400)
new_esEs20(xy32, xy402, ty_Int) → new_esEs18(xy32, xy402)
new_esEs12(Right(xy30), Right(xy400), eb, ty_Double) → new_esEs13(xy30, xy400)
new_esEs12(Right(xy30), Left(xy400), eb, cf) → False
new_esEs12(Left(xy30), Right(xy400), eb, cf) → False
new_esEs6(xy30, xy400, app(ty_Maybe, ce)) → new_esEs19(xy30, xy400, ce)
new_esEs19(Just(xy30), Nothing, bbg) → False
new_esEs19(Nothing, Just(xy400), bbg) → False
new_esEs25(xy31, xy401, app(app(app(ty_@3, bdh), bea), beb)) → new_esEs11(xy31, xy401, bdh, bea, beb)
new_esEs20(xy32, xy402, app(app(app(ty_@3, gd), ge), gf)) → new_esEs11(xy32, xy402, gd, ge, gf)
new_esEs6(xy30, xy400, ty_@0) → new_esEs7(xy30, xy400)
new_esEs19(Just(xy30), Just(xy400), ty_Float) → new_esEs16(xy30, xy400)
new_esEs19(Nothing, Nothing, bbg) → True
new_esEs12(Right(xy30), Right(xy400), eb, ty_Float) → new_esEs16(xy30, xy400)
new_esEs20(xy32, xy402, app(app(ty_@2, gb), gc)) → new_esEs10(xy32, xy402, gb, gc)
new_esEs12(Right(xy30), Right(xy400), eb, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs10(@2(xy30, xy31), @2(xy400, xy401), bdc, bdd) → new_asAs(new_esEs26(xy30, xy400, bdc), new_esEs25(xy31, xy401, bdd))
new_esEs22(xy30, xy400, ty_Double) → new_esEs13(xy30, xy400)
new_esEs26(xy30, xy400, ty_Integer) → new_esEs14(xy30, xy400)
new_esEs6(xy30, xy400, app(app(app(ty_@3, bg), bh), ca)) → new_esEs11(xy30, xy400, bg, bh, ca)
new_esEs12(Left(xy30), Left(xy400), app(app(ty_Either, df), dg), cf) → new_esEs12(xy30, xy400, df, dg)
new_esEs6(xy30, xy400, app(ty_Ratio, bd)) → new_esEs9(xy30, xy400, bd)
new_esEs12(Right(xy30), Right(xy400), eb, ty_Integer) → new_esEs14(xy30, xy400)
new_esEs12(Left(xy30), Left(xy400), ty_Float, cf) → new_esEs16(xy30, xy400)
new_esEs12(Left(xy30), Left(xy400), app(ty_Maybe, ea), cf) → new_esEs19(xy30, xy400, ea)
new_primEqNat0(Zero, Succ(xy4000)) → False
new_primEqNat0(Succ(xy300), Zero) → False
new_esEs4(xy3, xy40, app(ty_[], bc)) → new_esEs5(xy3, xy40, bc)
new_esEs12(Left(xy30), Left(xy400), app(app(app(ty_@3, dc), dd), de), cf) → new_esEs11(xy30, xy400, dc, dd, de)
new_esEs20(xy32, xy402, ty_@0) → new_esEs7(xy32, xy402)
new_esEs12(Right(xy30), Right(xy400), eb, app(ty_[], fc)) → new_esEs5(xy30, xy400, fc)
new_esEs12(Right(xy30), Right(xy400), eb, app(ty_Maybe, fd)) → new_esEs19(xy30, xy400, fd)
new_esEs20(xy32, xy402, app(ty_[], ha)) → new_esEs5(xy32, xy402, ha)
new_esEs25(xy31, xy401, ty_@0) → new_esEs7(xy31, xy401)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs12(Left(xy30), Left(xy400), ty_Integer, cf) → new_esEs14(xy30, xy400)
new_esEs12(Left(xy30), Left(xy400), ty_Double, cf) → new_esEs13(xy30, xy400)
new_esEs15(True, False) → False
new_esEs15(False, True) → False
new_esEs16(Float(xy30, xy31), Float(xy400, xy401)) → new_esEs18(new_sr(xy30, xy400), new_sr(xy31, xy401))
new_esEs26(xy30, xy400, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs11(xy30, xy400, bfb, bfc, bfd)
new_esEs25(xy31, xy401, ty_Integer) → new_esEs14(xy31, xy401)
new_esEs21(xy31, xy401, ty_Int) → new_esEs18(xy31, xy401)
new_esEs26(xy30, xy400, ty_Char) → new_esEs8(xy30, xy400)
new_esEs18(xy3, xy40) → new_primEqInt(xy3, xy40)
new_esEs14(Integer(xy30), Integer(xy400)) → new_primEqInt(xy30, xy400)
new_esEs4(xy3, xy40, ty_Integer) → new_esEs14(xy3, xy40)
new_esEs12(Right(xy30), Right(xy400), eb, app(app(app(ty_@3, ef), eg), eh)) → new_esEs11(xy30, xy400, ef, eg, eh)
new_esEs17(LT, LT) → True
new_esEs22(xy30, xy400, app(ty_[], bbe)) → new_esEs5(xy30, xy400, bbe)
new_esEs22(xy30, xy400, ty_Char) → new_esEs8(xy30, xy400)
new_sr(Neg(xy310), Neg(xy4010)) → Pos(new_primMulNat0(xy310, xy4010))
new_esEs12(Right(xy30), Right(xy400), eb, app(app(ty_@2, ed), ee)) → new_esEs10(xy30, xy400, ed, ee)
new_esEs19(Just(xy30), Just(xy400), ty_Double) → new_esEs13(xy30, xy400)
new_esEs12(Left(xy30), Left(xy400), ty_Ordering, cf) → new_esEs17(xy30, xy400)
new_sr(Pos(xy310), Pos(xy4010)) → Pos(new_primMulNat0(xy310, xy4010))
new_asAs(False, xy26) → False
new_esEs25(xy31, xy401, app(ty_[], bee)) → new_esEs5(xy31, xy401, bee)
new_esEs25(xy31, xy401, app(ty_Ratio, bde)) → new_esEs9(xy31, xy401, bde)
new_esEs22(xy30, xy400, ty_Int) → new_esEs18(xy30, xy400)
new_primEqNat0(Zero, Zero) → True
new_esEs22(xy30, xy400, app(app(ty_Either, bbc), bbd)) → new_esEs12(xy30, xy400, bbc, bbd)
new_esEs6(xy30, xy400, ty_Double) → new_esEs13(xy30, xy400)
new_primMulNat0(Succ(xy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy40100)) → Zero
new_esEs19(Just(xy30), Just(xy400), app(ty_Ratio, bbh)) → new_esEs9(xy30, xy400, bbh)
new_esEs12(Left(xy30), Left(xy400), app(ty_Ratio, cg), cf) → new_esEs9(xy30, xy400, cg)
new_esEs19(Just(xy30), Just(xy400), app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs11(xy30, xy400, bcc, bcd, bce)
new_esEs20(xy32, xy402, ty_Float) → new_esEs16(xy32, xy402)
new_esEs20(xy32, xy402, app(ty_Maybe, hb)) → new_esEs19(xy32, xy402, hb)
new_esEs26(xy30, xy400, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs26(xy30, xy400, app(ty_Ratio, beg)) → new_esEs9(xy30, xy400, beg)
new_esEs6(xy30, xy400, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs26(xy30, xy400, app(app(ty_@2, beh), bfa)) → new_esEs10(xy30, xy400, beh, bfa)
new_esEs21(xy31, xy401, ty_@0) → new_esEs7(xy31, xy401)
new_esEs19(Just(xy30), Just(xy400), ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs19(Just(xy30), Just(xy400), ty_@0) → new_esEs7(xy30, xy400)
new_esEs19(Just(xy30), Just(xy400), ty_Integer) → new_esEs14(xy30, xy400)
new_esEs22(xy30, xy400, ty_@0) → new_esEs7(xy30, xy400)
new_esEs6(xy30, xy400, ty_Float) → new_esEs16(xy30, xy400)
new_esEs26(xy30, xy400, app(ty_[], bfg)) → new_esEs5(xy30, xy400, bfg)
new_primPlusNat0(Succ(xy270), xy40100) → Succ(Succ(new_primPlusNat1(xy270, xy40100)))
new_esEs25(xy31, xy401, ty_Float) → new_esEs16(xy31, xy401)
new_esEs11(@3(xy30, xy31, xy32), @3(xy400, xy401, xy402), ff, fg, fh) → new_asAs(new_esEs22(xy30, xy400, ff), new_asAs(new_esEs21(xy31, xy401, fg), new_esEs20(xy32, xy402, fh)))
new_esEs17(EQ, LT) → False
new_esEs17(LT, EQ) → False
new_esEs20(xy32, xy402, ty_Integer) → new_esEs14(xy32, xy402)
new_esEs12(Left(xy30), Left(xy400), ty_Int, cf) → new_esEs18(xy30, xy400)
new_esEs12(Left(xy30), Left(xy400), app(ty_[], dh), cf) → new_esEs5(xy30, xy400, dh)
new_esEs24(xy30, xy400, ty_Integer) → new_esEs14(xy30, xy400)
new_esEs22(xy30, xy400, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs4(xy3, xy40, app(app(ty_Either, eb), cf)) → new_esEs12(xy3, xy40, eb, cf)
new_esEs22(xy30, xy400, ty_Float) → new_esEs16(xy30, xy400)
new_primEqInt(Neg(Succ(xy300)), Neg(Succ(xy4000))) → new_primEqNat0(xy300, xy4000)
new_esEs22(xy30, xy400, app(ty_Maybe, bbf)) → new_esEs19(xy30, xy400, bbf)
new_esEs15(True, True) → True
new_esEs4(xy3, xy40, ty_Double) → new_esEs13(xy3, xy40)
new_primPlusNat1(Zero, Succ(xy401000)) → Succ(xy401000)
new_primPlusNat1(Succ(xy2700), Zero) → Succ(xy2700)
new_esEs19(Just(xy30), Just(xy400), ty_Int) → new_esEs18(xy30, xy400)
new_esEs12(Right(xy30), Right(xy400), eb, ty_@0) → new_esEs7(xy30, xy400)
new_esEs21(xy31, xy401, app(ty_Ratio, hc)) → new_esEs9(xy31, xy401, hc)
new_esEs20(xy32, xy402, app(ty_Ratio, ga)) → new_esEs9(xy32, xy402, ga)
new_esEs4(xy3, xy40, ty_Bool) → new_esEs15(xy3, xy40)
new_esEs4(xy3, xy40, ty_Char) → new_esEs8(xy3, xy40)
new_esEs26(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs21(xy31, xy401, ty_Char) → new_esEs8(xy31, xy401)
new_esEs25(xy31, xy401, ty_Int) → new_esEs18(xy31, xy401)
new_esEs22(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(xy3, xy40, ty_Float) → new_esEs16(xy3, xy40)
new_esEs17(EQ, EQ) → True
new_esEs12(Right(xy30), Right(xy400), eb, app(app(ty_Either, fa), fb)) → new_esEs12(xy30, xy400, fa, fb)
new_esEs25(xy31, xy401, app(app(ty_Either, bec), bed)) → new_esEs12(xy31, xy401, bec, bed)
new_esEs19(Just(xy30), Just(xy400), app(app(ty_@2, bca), bcb)) → new_esEs10(xy30, xy400, bca, bcb)
new_primEqInt(Neg(Succ(xy300)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy4000))) → False
new_esEs20(xy32, xy402, ty_Bool) → new_esEs15(xy32, xy402)
new_esEs22(xy30, xy400, app(app(ty_@2, baf), bag)) → new_esEs10(xy30, xy400, baf, bag)
new_esEs12(Right(xy30), Right(xy400), eb, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs19(Just(xy30), Just(xy400), app(ty_Maybe, bda)) → new_esEs19(xy30, xy400, bda)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs25(xy31, xy401, app(app(ty_@2, bdf), bdg)) → new_esEs10(xy31, xy401, bdf, bdg)
new_esEs12(Left(xy30), Left(xy400), ty_Char, cf) → new_esEs8(xy30, xy400)
new_asAs(True, xy26) → xy26
new_esEs23(xy31, xy401, ty_Integer) → new_esEs14(xy31, xy401)
new_primMulNat0(Succ(xy3100), Succ(xy40100)) → new_primPlusNat0(new_primMulNat0(xy3100, Succ(xy40100)), xy40100)
new_esEs4(xy3, xy40, app(ty_Ratio, bdb)) → new_esEs9(xy3, xy40, bdb)
new_esEs4(xy3, xy40, ty_@0) → new_esEs7(xy3, xy40)
new_esEs17(GT, GT) → True
new_esEs6(xy30, xy400, app(app(ty_Either, cb), cc)) → new_esEs12(xy30, xy400, cb, cc)
new_primEqInt(Pos(Succ(xy300)), Pos(Succ(xy4000))) → new_primEqNat0(xy300, xy4000)
new_esEs4(xy3, xy40, app(ty_Maybe, bbg)) → new_esEs19(xy3, xy40, bbg)
new_esEs22(xy30, xy400, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs11(xy30, xy400, bah, bba, bbb)
new_esEs25(xy31, xy401, app(ty_Maybe, bef)) → new_esEs19(xy31, xy401, bef)
new_esEs17(GT, LT) → False
new_esEs17(LT, GT) → False
new_esEs24(xy30, xy400, ty_Int) → new_esEs18(xy30, xy400)
new_esEs8(Char(xy30), Char(xy400)) → new_primEqNat0(xy30, xy400)
new_esEs6(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_primEqNat0(Succ(xy300), Succ(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs17(GT, EQ) → False
new_esEs17(EQ, GT) → False
new_esEs6(xy30, xy400, app(ty_[], cd)) → new_esEs5(xy30, xy400, cd)
new_esEs19(Just(xy30), Just(xy400), ty_Bool) → new_esEs15(xy30, xy400)
new_esEs19(Just(xy30), Just(xy400), app(ty_[], bch)) → new_esEs5(xy30, xy400, bch)
new_esEs7(@0, @0) → True
new_esEs21(xy31, xy401, app(app(app(ty_@3, hf), hg), hh)) → new_esEs11(xy31, xy401, hf, hg, hh)
new_esEs12(Right(xy30), Right(xy400), eb, app(ty_Ratio, ec)) → new_esEs9(xy30, xy400, ec)
new_esEs20(xy32, xy402, ty_Char) → new_esEs8(xy32, xy402)
new_esEs19(Just(xy30), Just(xy400), ty_Char) → new_esEs8(xy30, xy400)
new_esEs6(xy30, xy400, ty_Char) → new_esEs8(xy30, xy400)
new_esEs21(xy31, xy401, ty_Float) → new_esEs16(xy31, xy401)
new_esEs12(Left(xy30), Left(xy400), app(app(ty_@2, da), db), cf) → new_esEs10(xy30, xy400, da, db)
new_esEs4(xy3, xy40, ty_Ordering) → new_esEs17(xy3, xy40)
new_esEs21(xy31, xy401, app(app(ty_@2, hd), he)) → new_esEs10(xy31, xy401, hd, he)
new_primEqInt(Pos(Succ(xy300)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy4000))) → False
new_esEs21(xy31, xy401, ty_Bool) → new_esEs15(xy31, xy401)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs15(False, False) → True
new_esEs12(Right(xy30), Right(xy400), eb, ty_Char) → new_esEs8(xy30, xy400)

The set Q consists of the following terms:

new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs7(@0, @0)
new_esEs12(Right(x0), Right(x1), x2, ty_Float)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, ty_Double)
new_esEs8(Char(x0), Char(x1))
new_esEs26(x0, x1, ty_Int)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs26(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs21(x0, x1, ty_Ordering)
new_esEs19(Just(x0), Just(x1), ty_Char)
new_esEs19(Nothing, Just(x0), x1)
new_esEs6(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, LT)
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Left(x0), Left(x1), ty_Float, x2)
new_esEs4(x0, x1, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Just(x0), Just(x1), ty_Integer)
new_esEs15(True, False)
new_esEs15(False, True)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs15(True, True)
new_esEs21(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Char)
new_esEs5(:(x0, x1), [], x2)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs19(Just(x0), Nothing, x1)
new_esEs12(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs12(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs6(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs15(False, False)
new_primPlusNat0(Succ(x0), x1)
new_esEs5([], :(x0, x1), x2)
new_esEs6(x0, x1, ty_Char)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Just(x0), Just(x1), ty_Ordering)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs20(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs12(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs12(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs14(Integer(x0), Integer(x1))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs18(x0, x1)
new_esEs12(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_@0)
new_esEs17(GT, GT)
new_esEs20(x0, x1, ty_@0)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(x0, x1, ty_Double)
new_esEs20(x0, x1, ty_Integer)
new_esEs19(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs12(Right(x0), Right(x1), x2, ty_Double)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs19(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs9(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(x0, x1, ty_Ordering)
new_esEs12(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs12(Right(x0), Left(x1), x2, x3)
new_esEs12(Left(x0), Right(x1), x2, x3)
new_esEs12(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Zero, Zero)
new_esEs6(x0, x1, ty_Ordering)
new_esEs21(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
new_esEs6(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5([], [], x0)
new_esEs6(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Int)
new_esEs12(Left(x0), Left(x1), ty_Int, x2)
new_esEs19(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Just(x0), Just(x1), ty_Bool)
new_esEs12(Right(x0), Right(x1), x2, ty_Int)
new_esEs12(Left(x0), Left(x1), ty_@0, x2)
new_esEs26(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs19(Just(x0), Just(x1), ty_@0)
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Int)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs12(Left(x0), Left(x1), ty_Integer, x2)
new_esEs19(Just(x0), Just(x1), ty_Float)
new_esEs4(x0, x1, ty_Bool)
new_primMulNat0(Zero, Succ(x0))
new_esEs19(Just(x0), Just(x1), app(ty_Ratio, x2))
new_asAs(False, x0)
new_esEs19(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Succ(x0))
new_esEs12(Right(x0), Right(x1), x2, ty_@0)
new_esEs12(Right(x0), Right(x1), x2, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_asAs(True, x0)
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_@0)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Integer)
new_esEs12(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs25(x0, x1, ty_Bool)
new_primPlusNat1(Zero, Zero)
new_esEs12(Left(x0), Left(x1), ty_Double, x2)
new_esEs12(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs6(x0, x1, ty_@0)
new_esEs19(Just(x0), Just(x1), ty_Double)
new_esEs12(Right(x0), Right(x1), x2, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs21(x0, x1, ty_Bool)
new_esEs12(Left(x0), Left(x1), ty_Char, x2)
new_esEs19(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs16(Float(x0, x1), Float(x2, x3))
new_esEs12(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs12(Right(x0), Right(x1), x2, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs17(EQ, EQ)
new_esEs17(LT, EQ)
new_esEs17(EQ, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Double)
new_esEs19(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Int)
new_esEs13(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: